'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(x)) -> mark(f(f(x)))
, chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, tp(mark(x)) ->
tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ active^#(f(x)) -> c_0(f^#(f(x)))
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))
, chk^#(no(c())) -> c_3(active^#(c()))
, mat^#(f(x), c()) -> c_4()
, f^#(active(x)) -> c_5(active^#(f(x)))
, f^#(no(x)) -> c_6(f^#(x))
, f^#(mark(x)) -> c_7(f^#(x))
, tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
The usable rules are:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))}
The estimated dependency graph contains the following edges:
{active^#(f(x)) -> c_0(f^#(f(x)))}
==> {f^#(mark(x)) -> c_7(f^#(x))}
{active^#(f(x)) -> c_0(f^#(f(x)))}
==> {f^#(no(x)) -> c_6(f^#(x))}
{active^#(f(x)) -> c_0(f^#(f(x)))}
==> {f^#(active(x)) -> c_5(active^#(f(x)))}
{chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
==> {f^#(mark(x)) -> c_7(f^#(x))}
{chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
==> {f^#(no(x)) -> c_6(f^#(x))}
{chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
==> {f^#(active(x)) -> c_5(active^#(f(x)))}
{f^#(active(x)) -> c_5(active^#(f(x)))}
==> {active^#(f(x)) -> c_0(f^#(f(x)))}
{f^#(no(x)) -> c_6(f^#(x))}
==> {f^#(mark(x)) -> c_7(f^#(x))}
{f^#(no(x)) -> c_6(f^#(x))}
==> {f^#(no(x)) -> c_6(f^#(x))}
{f^#(no(x)) -> c_6(f^#(x))}
==> {f^#(active(x)) -> c_5(active^#(f(x)))}
{f^#(mark(x)) -> c_7(f^#(x))}
==> {f^#(mark(x)) -> c_7(f^#(x))}
{f^#(mark(x)) -> c_7(f^#(x))}
==> {f^#(no(x)) -> c_6(f^#(x))}
{f^#(mark(x)) -> c_7(f^#(x))}
==> {f^#(active(x)) -> c_5(active^#(f(x)))}
{tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
==> {tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
We consider the following path(s):
1) { chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, active^#(f(x)) -> c_0(f^#(f(x)))
, f^#(active(x)) -> c_5(active^#(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))
, f^#(no(x)) -> c_6(f^#(x))}
The usable rules for this path are the following:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, active^#(f(x)) -> c_0(f^#(f(x)))
, f^#(active(x)) -> c_5(active^#(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))
, f^#(no(x)) -> c_6(f^#(x))}
Details:
We apply the weight gap principle, strictly orienting the rules
{f^#(mark(x)) -> c_7(f^#(x))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(mark(x)) -> c_7(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [8]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [1] x1 + [1]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(x)) -> mark(f(f(x)))}
and weakly orienting the rules
{f^#(mark(x)) -> c_7(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(x)) -> mark(f(f(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [4]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [1] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(f(x)) -> c_0(f^#(f(x)))}
and weakly orienting the rules
{ active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(f(x)) -> c_0(f^#(f(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [1] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(active(x)) -> c_5(active^#(f(x)))}
and weakly orienting the rules
{ active^#(f(x)) -> c_0(f^#(f(x)))
, active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(active(x)) -> c_5(active^#(f(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [1]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [7]
c_0(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [7]
chk^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [1]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{mat(f(x), c()) -> no(c())}
and weakly orienting the rules
{ f^#(active(x)) -> c_5(active^#(f(x)))
, active^#(f(x)) -> c_0(f^#(f(x)))
, active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{mat(f(x), c()) -> no(c())}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [8]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [2]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [10]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
and weakly orienting the rules
{ mat(f(x), c()) -> no(c())
, f^#(active(x)) -> c_5(active^#(f(x)))
, active^#(f(x)) -> c_0(f^#(f(x)))
, active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [9]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [8]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [1] x1 + [9]
c_1(x1) = [1] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [2]
c_7(x1) = [1] x1 + [1]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{chk(no(c())) -> active(c())}
and weakly orienting the rules
{ chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat(f(x), c()) -> no(c())
, f^#(active(x)) -> c_5(active^#(f(x)))
, active^#(f(x)) -> c_0(f^#(f(x)))
, active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{chk(no(c())) -> active(c())}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [2]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [1]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [1]
chk^#(x1) = [1] x1 + [3]
c_1(x1) = [1] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [3]
c_7(x1) = [1] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(no(x)) -> c_6(f^#(x))}
and weakly orienting the rules
{ chk(no(c())) -> active(c())
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat(f(x), c()) -> no(c())
, f^#(active(x)) -> c_5(active^#(f(x)))
, active^#(f(x)) -> c_0(f^#(f(x)))
, active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(no(x)) -> c_6(f^#(x))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [12]
mat(x1, x2) = [1] x1 + [1] x2 + [12]
X() = [0]
y() = [0]
c() = [7]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [8]
c_0(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [8]
chk^#(x1) = [1] x1 + [15]
c_1(x1) = [1] x1 + [6]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [1] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{mat(f(x), f(y())) -> f(mat(x, y()))}
and weakly orienting the rules
{ f^#(no(x)) -> c_6(f^#(x))
, chk(no(c())) -> active(c())
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat(f(x), c()) -> no(c())
, f^#(active(x)) -> c_5(active^#(f(x)))
, active^#(f(x)) -> c_0(f^#(f(x)))
, active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{mat(f(x), f(y())) -> f(mat(x, y()))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [4]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [0]
no(x1) = [1] x1 + [7]
mat(x1, x2) = [1] x1 + [1] x2 + [6]
X() = [7]
y() = [5]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [1] x1 + [15]
c_1(x1) = [1] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ mat(f(x), f(y())) -> f(mat(x, y()))
, f^#(no(x)) -> c_6(f^#(x))
, chk(no(c())) -> active(c())
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat(f(x), c()) -> no(c())
, f^#(active(x)) -> c_5(active^#(f(x)))
, active^#(f(x)) -> c_0(f^#(f(x)))
, active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ mat(f(x), f(y())) -> f(mat(x, y()))
, f^#(no(x)) -> c_6(f^#(x))
, chk(no(c())) -> active(c())
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat(f(x), c()) -> no(c())
, f^#(active(x)) -> c_5(active^#(f(x)))
, active^#(f(x)) -> c_0(f^#(f(x)))
, active(f(x)) -> mark(f(f(x)))
, f^#(mark(x)) -> c_7(f^#(x))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(2) -> 2
, no_0(2) -> 2
, X_0() -> 2
, y_0() -> 2
, c_0() -> 2
, active^#_0(2) -> 1
, f^#_0(2) -> 1
, chk^#_0(2) -> 1
, c_6_0(1) -> 1
, c_7_0(1) -> 1}
2) {chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
The usable rules for this path are the following:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{active(f(x)) -> mark(f(f(x)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(x)) -> mark(f(f(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [2]
chk^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
and weakly orienting the rules
{active(f(x)) -> mark(f(f(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [1] x1 + [9]
c_1(x1) = [1] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
and weakly orienting the rules
{ chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, active(f(x)) -> mark(f(f(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [3]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [2]
chk(x1) = [1] x1 + [2]
no(x1) = [1] x1 + [1]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [6]
chk^#(x1) = [1] x1 + [8]
c_1(x1) = [1] x1 + [1]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{chk(no(c())) -> active(c())}
and weakly orienting the rules
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, active(f(x)) -> mark(f(f(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{chk(no(c())) -> active(c())}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [9]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [0]
no(x1) = [1] x1 + [12]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [10]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [2]
chk^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [2]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{mat(f(x), f(y())) -> f(mat(x, y()))}
and weakly orienting the rules
{ chk(no(c())) -> active(c())
, chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, active(f(x)) -> mark(f(f(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{mat(f(x), f(y())) -> f(mat(x, y()))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [8]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [0]
no(x1) = [1] x1 + [15]
mat(x1, x2) = [1] x1 + [1] x2 + [2]
X() = [0]
y() = [15]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [4]
chk^#(x1) = [1] x1 + [9]
c_1(x1) = [1] x1 + [2]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, active(f(x)) -> mark(f(f(x)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, chk^#(no(f(x))) ->
c_1(f^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, active(f(x)) -> mark(f(f(x)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(7) -> 3
, mark_0(8) -> 3
, mark_0(9) -> 3
, no_0(3) -> 5
, no_0(5) -> 5
, no_0(7) -> 5
, no_0(8) -> 5
, no_0(9) -> 5
, X_0() -> 7
, y_0() -> 8
, c_0() -> 9
, f^#_0(3) -> 13
, f^#_0(5) -> 13
, f^#_0(7) -> 13
, f^#_0(8) -> 13
, f^#_0(9) -> 13
, chk^#_0(3) -> 14
, chk^#_0(5) -> 14
, chk^#_0(7) -> 14
, chk^#_0(8) -> 14
, chk^#_0(9) -> 14}
3) {tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
The usable rules for this path are the following:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, chk(no(c())) -> active(c())
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))
, tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ mat(f(x), c()) -> no(c())
, active(f(x)) -> mark(f(f(x)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ mat(f(x), c()) -> no(c())
, active(f(x)) -> mark(f(f(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [2]
X() = [0]
y() = [2]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [1] x1 + [15]
c_8(x1) = [1] x1 + [15]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
and weakly orienting the rules
{ mat(f(x), c()) -> no(c())
, active(f(x)) -> mark(f(f(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [9]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [8]
chk(x1) = [1] x1 + [1]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [1] x1 + [8]
c_8(x1) = [1] x1 + [6]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{mat(f(x), f(y())) -> f(mat(x, y()))}
and weakly orienting the rules
{ tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat(f(x), c()) -> no(c())
, active(f(x)) -> mark(f(f(x)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{mat(f(x), f(y())) -> f(mat(x, y()))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [12]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [11]
chk(x1) = [1] x1 + [0]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [0]
X() = [0]
y() = [6]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [1] x1 + [3]
c_8(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, chk(no(c())) -> active(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ mat(f(x), f(y())) -> f(mat(x, y()))
, tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat(f(x), c()) -> no(c())
, active(f(x)) -> mark(f(f(x)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ chk(no(f(x))) ->
f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
, chk(no(c())) -> active(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ mat(f(x), f(y())) -> f(mat(x, y()))
, tp^#(mark(x)) ->
c_8(tp^#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))))
, mat(f(x), c()) -> no(c())
, active(f(x)) -> mark(f(f(x)))}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ active_1(37) -> 25
, active_2(52) -> 39
, f_0(7) -> 36
, f_0(28) -> 27
, f_0(29) -> 28
, f_0(30) -> 29
, f_0(31) -> 30
, f_0(32) -> 31
, f_0(33) -> 32
, f_0(34) -> 33
, f_0(35) -> 34
, f_0(36) -> 35
, f_1(42) -> 41
, f_1(43) -> 42
, f_1(44) -> 43
, f_1(45) -> 44
, f_1(46) -> 45
, f_1(47) -> 46
, f_1(48) -> 47
, f_1(49) -> 48
, f_1(50) -> 49
, f_1(51) -> 50
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(7) -> 3
, mark_0(8) -> 3
, mark_0(9) -> 3
, chk_0(26) -> 25
, chk_1(40) -> 39
, no_0(3) -> 5
, no_0(5) -> 5
, no_0(7) -> 5
, no_0(8) -> 5
, no_0(9) -> 5
, no_0(9) -> 26
, no_1(37) -> 40
, mat_0(27, 3) -> 26
, mat_0(27, 5) -> 26
, mat_0(27, 7) -> 26
, mat_0(27, 8) -> 26
, mat_0(27, 9) -> 26
, mat_1(41, 3) -> 40
, mat_1(41, 5) -> 40
, mat_1(41, 7) -> 40
, mat_1(41, 8) -> 40
, mat_1(41, 9) -> 40
, X_0() -> 7
, X_1() -> 51
, y_0() -> 8
, c_0() -> 9
, c_1() -> 37
, c_2() -> 52
, tp^#_0(3) -> 23
, tp^#_0(5) -> 23
, tp^#_0(7) -> 23
, tp^#_0(8) -> 23
, tp^#_0(9) -> 23
, tp^#_0(25) -> 24
, tp^#_1(39) -> 38
, c_8_0(24) -> 23
, c_8_1(38) -> 23}
4) {mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
The usable rules for this path are the following:
{ mat(f(x), f(y())) -> f(mat(x, y()))
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ mat(f(x), f(y())) -> f(mat(x, y()))
, mat(f(x), c()) -> no(c())
, f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))
, active(f(x)) -> mark(f(f(x)))
, mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
Details:
We apply the weight gap principle, strictly orienting the rules
{mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [0] x1 + [0]
no(x1) = [1] x1 + [1]
mat(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [1] x1 + [1] x2 + [9]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{mat(f(x), c()) -> no(c())}
and weakly orienting the rules
{mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{mat(f(x), c()) -> no(c())}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [1] x1 + [0]
chk(x1) = [0] x1 + [0]
no(x1) = [1] x1 + [1]
mat(x1, x2) = [1] x1 + [1] x2 + [9]
X() = [0]
y() = [8]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [0]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [1] x1 + [1] x2 + [15]
c_2(x1) = [1] x1 + [4]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{mat(f(x), f(y())) -> f(mat(x, y()))}
and weakly orienting the rules
{ mat(f(x), c()) -> no(c())
, mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{mat(f(x), f(y())) -> f(mat(x, y()))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [4]
mark(x1) = [1] x1 + [12]
chk(x1) = [0] x1 + [0]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [1]
X() = [0]
y() = [8]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [8]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [1] x1 + [1] x2 + [11]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(f(x)) -> mark(f(f(x)))}
and weakly orienting the rules
{ mat(f(x), f(y())) -> f(mat(x, y()))
, mat(f(x), c()) -> no(c())
, mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(f(x)) -> mark(f(f(x)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [2]
f(x1) = [1] x1 + [1]
mark(x1) = [1] x1 + [0]
chk(x1) = [0] x1 + [0]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [1] x1 + [1] x2 + [4]
X() = [0]
y() = [0]
c() = [12]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [1] x1 + [1] x2 + [5]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ active(f(x)) -> mark(f(f(x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, mat(f(x), c()) -> no(c())
, mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ f(active(x)) -> active(f(x))
, f(no(x)) -> no(f(x))
, f(mark(x)) -> mark(f(x))}
Weak Rules:
{ active(f(x)) -> mark(f(f(x)))
, mat(f(x), f(y())) -> f(mat(x, y()))
, mat(f(x), c()) -> no(c())
, mat^#(f(x), f(y())) -> c_2(f^#(mat(x, y())))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, mark_0(9) -> 3
, no_0(3) -> 5
, no_0(5) -> 5
, no_0(8) -> 5
, no_0(9) -> 5
, y_0() -> 8
, c_0() -> 9
, f^#_0(3) -> 13
, f^#_0(5) -> 13
, f^#_0(8) -> 13
, f^#_0(9) -> 13
, mat^#_0(3, 3) -> 16
, mat^#_0(3, 5) -> 16
, mat^#_0(3, 8) -> 16
, mat^#_0(3, 9) -> 16
, mat^#_0(5, 3) -> 16
, mat^#_0(5, 5) -> 16
, mat^#_0(5, 8) -> 16
, mat^#_0(5, 9) -> 16
, mat^#_0(8, 3) -> 16
, mat^#_0(8, 5) -> 16
, mat^#_0(8, 8) -> 16
, mat^#_0(8, 9) -> 16
, mat^#_0(9, 3) -> 16
, mat^#_0(9, 5) -> 16
, mat^#_0(9, 8) -> 16
, mat^#_0(9, 9) -> 16}
5) {chk^#(no(c())) -> c_3(active^#(c()))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
chk(x1) = [0] x1 + [0]
no(x1) = [0] x1 + [0]
mat(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {chk^#(no(c())) -> c_3(active^#(c()))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{chk^#(no(c())) -> c_3(active^#(c()))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{chk^#(no(c())) -> c_3(active^#(c()))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
chk(x1) = [0] x1 + [0]
no(x1) = [1] x1 + [0]
mat(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
chk^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {chk^#(no(c())) -> c_3(active^#(c()))}
Details:
The given problem does not contain any strict rules
6) {mat^#(f(x), c()) -> c_4()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
mark(x1) = [0] x1 + [0]
chk(x1) = [0] x1 + [0]
no(x1) = [0] x1 + [0]
mat(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {mat^#(f(x), c()) -> c_4()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{mat^#(f(x), c()) -> c_4()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{mat^#(f(x), c()) -> c_4()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
f(x1) = [1] x1 + [0]
mark(x1) = [0] x1 + [0]
chk(x1) = [0] x1 + [0]
no(x1) = [0] x1 + [0]
mat(x1, x2) = [0] x1 + [0] x2 + [0]
X() = [0]
y() = [0]
c() = [0]
tp(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
chk^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
mat^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4() = [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
tp^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {mat^#(f(x), c()) -> c_4()}
Details:
The given problem does not contain any strict rules